| Definitions | t  T, finite-prob-space, unit-fps, P  Q, qsum(a; b; j.E(j)), ||as||, l[i], l_all(L; T; x.P(x)), qle(r; s),  x:A. B(x), A c B, rng_sum(r; i; j; k.E(k)), mon_itop(g; lb; ub; i.E(i)), itop(op; id; lb; ub; i.E(i)), Y, if b then t else f fi , i <z j, tt, x f y, grp_op(g), t.1, t.2, add_grp_of_rng(r), rng_plus(r), qrng, r + s, ff, grp_id(g), rng_zero(r), hd(l), nth_tl(n;as), i  z j,   b, P   Q, A B, A, sq_type(T), guard(T), prop{i:l}, grp_leq(g; a; b),  b, grp_le(g), qadd_grp, q_le(r; s), bor(p; q), qpositive(r), r - s, r * s, True,   x. t(x), False, (x l),  x:A. B(x),  , decidable(P), P  Q, int_seg(i; j), x(s), lelt(i; j; k), subtype(S; T) |